The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...) in this paper makes clearer the relations betweenKC p ,H p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC p is given. (shrink)

We prove that every finitely axiomatizable extension of Heyting's intuitionistic logic has a corresponding cut-free Gentzen-type formulation. It is shown how one can use this result to find the corresponding normalizable natural deduction system and to give a criterion for separability of considered logic. Obviously, the question how to obtain an effective definition of a sequent calculus which corresponds to a concrete logic remains a separate problem for every logic.

In distinction from the well-known double-negation embeddings of the classical logic we consider some variants of single-negation embeddings and describe some classes of superintuitionistic first-order predicate logics in which the classical first-order calculus is interpretable in such a way. Also we find the minimal extensions of Heyting's logic in which the classical predicate logic can be embedded by means of these translations.